m, a, b:. a = b  (a = b mod m) 

latex

Definitions	a = b mod m, x:A. B(x), P  Q, Prop, t  T, T, True, b | a
Lemmas	any divs zero, divides wf, true wf, squash wf